T:Type, P:((T List)Prop).
(L:T List. Dec(P(L)))
 (L:T List.
 (P(L)  (L':T List. L'  L & P(L') & (L'':T List. L''  L'  P(L'')  L'' = L'))) 

latex

Definitions

t  T, x(s), x:A. B(x), l1  l2, P & Q, x:A. B(x), P  Q, False, A, AB, , P  Q, Dec(P), ||as||, ij, {T}, Prop, null(as), b, True, P  Q, P  Q, x. t(x), last(L), A & B, SQType(T), T, as @ bs

Lemmas

cons iseg, append wf, squash wf, iseg append iff, iseg weakening, cons one one, member wf, iseg append0, iseg transitivity, length append, last wf, iseg length, last lemma, decidable-exists-iseg, iseg nil, null wf2, iseg wf, and functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, assert of null, true wf, assert wf, ge wf, nat properties, decidable wf, nat wf, le wf, non neg length, length wf1, decidable assert, null wf